Nuprl Lemma : qmul-preserves-eq
11,40
postcript
pdf
a
,
b
,
c
:
. (
(
c
= 0
))
((
a
=
b
)
((
c
*
a
) = (
c
*
b
)
))
latex
Definitions
T
,
True
,
,
t
T
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qmul
one
qrng
,
qmul-qdiv-cancel2
,
qmul
ac
1
qrng
,
qmul
comm
qrng
,
true
wf
,
squash
wf
,
qdiv
wf
,
int
inc
rationals
,
not
wf
,
rationals
wf
,
qmul
wf
origin
a, b, c:
. (
(c = 0 
)) 
((a = b) 
((c * a) = (c * b) )) a, b, c:. ((c = 0 )) ((a = b) ((c * a) = (c * b) )) 
T
T Q Q Qx:A. B(x)
T